T:Type, f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x) 

latex

Definitions	P  Q, P & Q, P  Q, f^n, T, , , A, False, P  Q, AB, x:A. B(x), True, t  T
Lemmas	le wf, nat wf, true wf, squash wf, fun exp wf, nat plus inc, fun exp add1, nat plus wf